\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;$i$)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ ($\uparrow$kind($e$) $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ ((valtype($e$) $\subseteq$r (${\it conds}$(kind($e$)).1)) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\-\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ es{-}triggers(${\it es}$;$i$;${\it ds}$;${\it conds}$))) $\Rightarrow$ (loc($e$) = $i$))
\end{tabbing}